(* $Id$ *)

(** The following will be imported from the standard library in the future. *)

(* [&] decides the boolean conjunction. *)
deferred val & : (bool * bool) -> bool
where (forall (x, y). pre (&) (x, y))
  and (forall (x, y). post (&) (x, y) (true) <=> (x = true and y = true))

(* [+'] computes the addition between two integers. *)
deferred val +? : (int * int) -> int
where (forall (x, y). pre (+?) (x, y))
  and (forall (x, y, z). post (+?) (x, y) (z) <=> z = x + y)

(* [-'] computes the substraction between two integers. *)
deferred val -? : (int * int) -> int
where (forall (x, y). pre (-?) (x, y))
  and (forall (x, y, z). post (-?) (x, y) (z) <=> z = x - y)

(* [max] is the logical function that returns the maximum of two integers. *)
deferred logic max  : (int * int) ~> int
where forall (x, y). (x < y => max (x, y) = y) and (y <= x => max (x, y) = x)

(* [max'] is the implementation of the [max] logical function. *)
deferred val max? : (int * int) -> int
where (forall (x, y). pre (max?) (x, y))
  and (forall (x, y, z). post (max?) (x, y) (z) <=> z = max (x, y))

(* The bounded distance between two integers. *)
deferred predicate dist : (int * int * int) ~> prop
where forall (x, y, p). dist (x, y, p) <=> ((x - y >= (0 - p) and (x - y) <= p))

(* Comparison operators over integers. *)
deferred val <=?  : (int * int) -> bool where 
    (forall (x, y). (post (<=?) (x, y) (true)  <=> x <= y))
and (forall (x, y). (post (<=?) (x, y) (false) <=> not (x <= y)))
and (forall (x, y). pre (<=?) (x, y))

deferred val >=?  : (int * int) -> bool where 
    (forall (x, y). (post (>=?) (x, y) (true)  <=> x >= y))
and (forall (x, y). (post (>=?) (x, y) (false) <=> not (x >= y)))
and (forall (x, y). pre (>=?) (x, y)) 

deferred val >?   : (int * int) -> bool where 
    (forall (x, y). (post (>?) (x, y) (true)  <=> x > y))
and (forall (x, y). (post (>?) (x, y) (false) <=> not (x > y)))
and (forall (x, y). pre (>?) (x, y)) 

deferred val =?   : (int * int) -> bool
where (forall (x, y). pre ( =? ) (x, y))
  and (forall (x, y). post (=?) (x, y) (true) <=> x = y)
  and (forall (x, y). post (=?) (x, y) (false) <=> not (x = y))

(** Elements of the sets. *)

(* The type of the elements. *)
deferred type elt : *

(* Their equality is decidable. *)
deferred val =elt?  : (elt * elt) -> bool
where (forall x. pre (=elt?) (x))
  and (forall (x, y). post (=elt?) (x, y) (true) <=> x = y)
  and (forall (x, y). post (=elt?) (x, y) (false) <=> not (x = y))

(* There exists an order. *)
deferred predicate <elt : (elt * elt) ~> prop 
where (forall x. not (x <elt x))
  and (forall (x, y). (not (x <elt y) and not (x = y)) => y <elt x)
  and (forall (x, y, z). (x <elt y and y <elt z) => x <elt z)
  and (forall (x, y). (x <elt y) or (y <elt x) or (x = y))

(* This order is decidable. *)
deferred val <elt? : (elt * elt) -> bool where 
    (forall (x, y). (post (<elt?) (x, y) (true)  <=> x <elt y))
and (forall (x, y). (post (<elt?) (x, y) (false) <=> not (x <elt y)))
and (forall (x, y). pre (<elt?) (x, y)) 

(** The sets. *)

(* The type of an abstract set. *)
deferred type set : *

(* The membership predicate. *)
deferred predicate %in : (elt * set) ~> prop

(* The empty set. *)
deferred val empty : set
where forall x [x]. not (x %in empty)

deferred logic singleton : elt ~> set
where forall (x, y). x %in (singleton (y)) <=> (x = y)

deferred logic @ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 @ s2) <=> ((x %in s1) or (x %in s2))

deferred logic ^ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 ^ s2) <=> ((x %in s1) and (x %in s2))

deferred logic \\ : (set * set) ~> set
where forall (s1, s2, x). x %in (s1 \\ s2) <=> ((x %in s1) and not (x %in s2))

deferred predicate %C : (set * set) ~> prop
where forall (s1, s2). (s1 %C s2) <=> (forall x. (x %in s1) => (x %in s2))

deferred predicate disjoint : (set * set) ~> prop
where forall (s1, s2). disjoint (s1, s2) <=> ((forall y. y %in s1 => not (y %in s2)) and (forall y. y %in s2 => not (y %in s1)))

(* Extensional equality. *)
predicate === (s1, s2) = forall x. (x %in s1) <=> (x %in s2)

(* Extensionality axiom. *)
axiom: forall (s1, s2). (s1 === s2) <=> (s1 = s2) 

axiom union_subset : forall (s1, s2). s1 %C (s1 @ s2) 
axiom union_subset' : forall (s1, s2). s2 %C (s1 @ s2) 
axiom union_diff_ext: forall (s1, s2). s2 %C s1 => (((s1 \\ s2) @ s2) === s1)
axiom union_diff: forall (s1, s2). s2 %C s1 => ((s1 \\ s2) @ s2 = s1)
axiom flatten_union: forall (x, s1, s2, s3). x %in (s1 @ s2 @ s3) <=> (x %in s1 or x %in s2 or x %in s3) 
axiom flatten_union': forall (x, s1, s2, s3). x %in (s1 @ (s2 @ s3)) <=> (x %in s1 or x %in s2 or x %in s3) 
axiom transitive_subset: forall (s1, s2, s3). (s1 %C s2 and s2 %C s3) => s1 %C s3
axiom diff_empty_ext: forall s. (s \\ empty) === s
axiom diff_empty: forall s. (s \\ empty) = s
axiom diff_union2_ext : forall (s1, s2, s3). (s1 \\ (s2 @ s3)) === ((s1 \\ s2) \\ s3)
axiom diff_union2 : forall (s1, s2, s3). (s1 \\ (s2 @ s3)) = (s1 \\ s2) \\ s3
axiom diff_subset : forall (s1, s2). (s1 \\ s2) %C s1
axiom diff_singleton: forall (s, x). not (x %in (s \\ singleton (x)))
axiom diff_full_ext: forall s. (s \\ s) === empty
axiom diff_full: forall s. (s \\ s) = empty
axiom diff_disjoint_union: forall (s1, s2). disjoint (s1, s2) => (forall s3. (s1 @ s2) %C s3 => s1 %C (s3 \\ s2))

(* Inferior bound of a set. *)
predicate inf (x, s) = forall y. y %in s => x <elt y

axiom: forall (x, s1, s2). (inf (x, s1) and s2 %C s1) => inf (x, s2)
axiom: forall (x, s1, s2). (inf (x, s1 @ s2)) <=> (inf (x, s1) and inf (x, s2))
axiom: forall (s, x, y). (inf (x, s) and y <elt x) => inf (y, s)
axiom: forall (x, y). (inf (x, singleton (y)) <=> x <elt y)
axiom: forall (x, s). (inf (x, s) => not (x %in s))

(* The minimum is unique. *)
axiom: forall (a, m1, m2). 
      (m1 %in a and (forall y. (y %in a) => (m1 <elt y or m1 = y)) and
       m2 %in a and (forall y. (y %in a) => (m2 <elt y or m2 = y)))
      => m1 = m2 

(* Superior bound of a set. *)
predicate sup (x, s) = forall y. y %in s => y <elt x

axiom: forall (x, s1, s2). (sup (x, s1) and s2 %C s1) => sup (x, s2)
axiom: forall (x, s1, s2). (sup (x, s1 @ s2)) <=> (sup (x, s1) and sup (x, s2))
axiom: forall (s, x, y). (sup (x, s) and x <elt y) => sup (y, s)
axiom: forall (x, y). (sup (x, singleton (y)) <=> y <elt x)
axiom: forall (x, s). (sup (x, s) => not (x %in s))

(** Trees. *)

(* Inductive type for tree. *)
type tree =
  | Empty : tree
  | Node  : (int * tree * elt * tree) -> tree

(* The abstraction of trees to sets. *)
logic elements (t) = 
  | Empty -> empty
  | Node (h, l, x, r) -> elements (l) @ singleton (x) @ elements (r)

axiom root_in_elements: forall (h, l, x, r). x %in elements (Node (h, l, x, r))

axiom subl_in_elements: forall (h, l, x, r). 
  elements (l) %C elements (Node (h, l, x, r))

axiom subr_in_elements: forall (h, l, x, r). 
  elements (r) %C elements (Node (h, l, x, r))

axiom subl2_in_elements: forall (h, hl, ll, lx, lr, x, r). 
    elements (ll) %C elements (Node (h, Node (hl, ll, lx, lr), x, r))
and elements (lr) %C elements (Node (h, Node (hl, ll, lx, lr), x, r))

axiom subr2_in_elements: forall (h, l, x, hr, rl, rx, rr). 
  elements (rl) %C elements (Node (h, l, x, Node (hr, rl, rx, rr)))
and elements (rr) %C elements (Node (h, l, x, Node (hr, rl, rx, rr)))

(* Binary search trees. *)

inductive bst : tree ~> prop =
  | bst (Empty)
  | forall (h, l, x, r). 
      bst (l) and bst (r) and sup (x, elements (l)) and inf (x, elements (r))
      => bst (Node (h, l, x, r))

predicate bst_node (l, x, r) = 
   bst (l) and bst (r) and sup (x, elements (l)) and inf (x, elements (r))

axiom: forall (l, x, r). bst_node (l, x, r) => 
    ((disjoint (elements (l), elements (r))) 
 and (disjoint (elements (l), singleton (x)))
 and (disjoint (elements (r), singleton (x))))

axiom: forall (lh, ll, lx, lr, x, rh, rl, rx, rr). 
   bst_node (Node (lh, ll, lx, lr), x, Node (rh, rl, rx, rr)) =>
   (bst_node (ll, lx, lr) and bst_node (rl, rx, rr))

axiom: forall (l, x, h, rl, rx, rr).
   bst_node (l, x, Node (h, rl, rx, rr)) =>
   sup (rx, elements (l) @ singleton (x) @ elements (rl))

axiom: forall (h, ll, lx, lr, x, r).
   bst_node (Node (h, ll, lx, lr), x, r) =>
   inf (lx, elements (lr) @ singleton (x) @ elements (r))

axiom: forall (lh, ll, lx, lrh, lrl, lrx, lrr, x, r).
   bst_node (Node (lh, ll, lx, Node (lrh, lrl, lrx, lrr)), x, r) =>
   inf (lrx, elements (lrr) @ singleton (x) @ elements (r))

axiom: forall (h, l, x, rh, rlh, rll, rlx, rlr, rx, rr).
   bst_node (l, x, Node (rh, Node (rlh, rll, rlx, rlr), rx, rr)) =>
   sup (rlx, elements (l) @ singleton (x) @ elements (rll))

axiom: forall (h, l, x, r). bst (Node (h, l, x, r)) 
=> (forall y. ((y %in elements (Node (h, l, x, r))) and y <elt x) <=> y %in elements (l))

axiom: forall (h, l, x, r). bst (Node (h, l, x, r)) 
=> (forall y. ((y %in elements (Node (h, l, x, r))) and x <elt y) <=> y %in elements (r))

axiom: forall (h, l, x, r). bst_node (l, x, r) <=> bst (Node (h, l, x, r))

predicate hereditary_invariant (inv, s0, f) = 
  forall (x, s', accu'). 
    ((s' @ singleton (x)) %C s0 
    and not (x %in s') 
    and inv (accu', s' @ singleton (x))) =>
    (pre (f) (accu', x) 
     and (forall accu''. (post (f) (accu', x) (accu'') => inv (accu'', s'))))

lemma hereditary_invariant_subset: 
  forall (s, s0, inv, f). (s %C s0 and hereditary_invariant (inv, s0, f)) 
  => hereditary_invariant (inv, s, f)

predicate is_invariant (inv, s0, s1, f, accu) =
  s1 %C s0 and inv (accu, s0) and hereditary_invariant (inv, s0, f)

deferred logic cardinal : set ~> int
where cardinal (empty) = 0 
  and forall (x, s). not (x %in s) 
      => cardinal (s @ singleton (x)) = 1 + cardinal (s)

predicate cardinal_inv (t) = 
  fun (accu, s) -> accu + cardinal (s) = cardinal (elements(t))

let incr (x, z) returns y where (y = x + 1) = x +? 1

lemma is_hereditary_cardinal_inv: 
  forall t. hereditary_invariant (cardinal_inv (t), elements (t), incr)

let rec fold [s0, inv] (accu, t, f) 
where is_invariant (inv, s0, elements (t), f, accu) and bst (t)
returns accu' where inv (accu', s0 \\ elements (t)) =
  match t with
  | Empty -> accu
  | Node (_, l, x, r) -> 
     let accu_l = fold [s0, inv] (accu, l, f) in
     assert inv (accu_l, ((s0 \\ elements (l)) \\ singleton (x)) @ singleton (x)) in
     let accu_x = f (accu_l, x) in
     assert (elements (r) %C (s0 \\ (elements (l) @ singleton (x)))) in
        fold [s0 \\ (elements (l) @ singleton (x)), inv] (accu_x, r, f)
  end

let cardinal? (t) where bst (t) returns x where (x = cardinal (elements (t))) =
  fold [elements (t), cardinal_inv (t)] (0, t, incr)



